/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package alloy2code;

import alloy2code.Translator;
import edu.mit.csail.sdg.alloy4compiler.ast.Func;
import edu.mit.csail.sdg.alloy4compiler.ast.Sig;

/**
 *
 * @author Daniel
 */
public class CSharpTranslator implements Translator {
    
    public String PredTranslate(Func f) {
        return "public void "+f.label+"(){}";
    }

    public String PrecondTranslate(String pre) {
        return "/*"+pre+"*/";
    }

    public String PostcondTranslate(String pos) {
        return "/*"+pos+"*/";
    }

    public String SigTranslate(SigData s) {
        String tmp="class "+s.getSigName()+" {\n";
        for(Declaration d : s.getDecls()){
            if(d.mult.equals("set")){
                tmp+="\t HashSet<"+d.sigName+"> "+d.label+";\n";
            }
            if(d.mult.equals("one")){
                tmp+="\t "+d.sigName+" "+d.label+";\n \tContract.Requires("+d.label+" != null);\n";
            }
            if(d.mult.equals("lone")){
                tmp+="\t "+d.sigName+" "+d.label+";\n";
            }
            if(d.mult.endsWith("some")){
                tmp+="\t HashSet<"+d.sigName+"> "+d.label+";\n \tContract.Requires("+d.label+".Count()>=1);\n";
            }
        }
        tmp+="}";
        return tmp;
    }
}
